Nuprl Lemma : uni_sat_wf
9,38
postcript
pdf
T
:Type,
a
:
T
,
Q
:(
T
). (
a
= !
x
:
T
.
Q
(
x
))
latex
ProofTree
Definitions
P
Q
,
P
Q
,
x
(
s
)
,
a
= !
x
:
T
.
Q
(
x
)
,
t
T
,
,
x
:
A
.
B
(
x
)
origin
T:Type, a:T, Q:(T
). (a = !x:T. Q(x)) 
T:Type, a:T, Q:(T). (a = !x:T. Q(x))
Q
Q Tx:A. B(x)